Step of Proof: not_functionality_wrt_iff 9,38

Inference at * 
Iof proof for Lemma not functionality wrt iff:


  P,Q:. (P  Q ((P (Q)) 
latex

 by ((((((Unfold `not` 0) 
CollapseTHEN (GenUnivCD))
CollapseTHENM (HypBackchain))

CoCollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
C) inil_term))) 
latex


C.


Definitionst  T, P  Q, P  Q, A, P  Q, P  Q, , x:AB(x)
Lemmasiff wf, false wf

origin